The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
↳2 CdtProblem
↳3 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
↳4 CdtProblem
↳5 CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID))
↳6 CdtProblem
↳7 CdtKnowledgeProof (⇔)
↳8 CdtProblem
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
↳10 CdtProblem
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
↳12 CdtProblem
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
↳14 CdtProblem
↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
↳16 CdtProblem
↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
↳18 CdtProblem
↳19 CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication)
↳20 CdtProblem
↳21 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
↳22 CdtProblem
↳23 CdtUnreachableProof (⇔)
↳24 CdtProblem
↳25 CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication)
↳26 CdtProblem
↳27 CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID))
↳28 CdtProblem
↳29 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
↳30 CdtProblem
↳31 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
↳32 CdtProblem
↳33 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
↳34 CdtProblem
↳35 SIsEmptyProof (⇔)
↳36 BOUNDS(O(1), O(1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c15(QUOT(hd(sum(z0)), length(z0)), HD(sum(z0)), SUM(z0), LENGTH(z0))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c15(QUOT(hd(sum(z0)), length(z0)), HD(sum(z0)), SUM(z0), LENGTH(z0))
K tuples:none
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c15

(3) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(HD(sum(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(HD(sum(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
K tuples:none
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c

(5) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
K tuples:none
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c, c

(7) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c, c

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

LENGTH(:(z0, z1)) → c13(LENGTH(z1))
We considered the (Usable) Rules:

sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
hd(:(z0, z1)) → z0
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = [2] + [3]x1 + [2]x2   
POL(+'(x1, x2)) = 0   
POL(++(x1, x2)) = 0   
POL(++'(x1, x2)) = 0   
POL(-(x1, x2)) = [3] + [4]x1   
POL(-'(x1, x2)) = 0   
POL(0) = [3]   
POL(:(x1, x2)) = [1] + x2   
POL(AVG(x1)) = [4] + [2]x1   
POL(LENGTH(x1)) = [1] + x1   
POL(QUOT(x1, x2)) = [4]   
POL(SUM(x1)) = 0   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c11(x1, x2)) = x1 + x2   
POL(c13(x1)) = x1   
POL(c3(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1, x2, x3)) = x1 + x2 + x3   
POL(c9(x1)) = x1   
POL(hd(x1)) = [4]   
POL(length(x1)) = [3] + [3]x1   
POL(nil) = 0   
POL(s(x1)) = [2]   
POL(sum(x1)) = [5]   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c, c

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
We considered the (Usable) Rules:

sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
hd(:(z0, z1)) → z0
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = 0   
POL(+'(x1, x2)) = 0   
POL(++(x1, x2)) = [4]x2   
POL(++'(x1, x2)) = 0   
POL(-(x1, x2)) = [4] + [2]x1 + [5]x2   
POL(-'(x1, x2)) = 0   
POL(0) = [3]   
POL(:(x1, x2)) = [1] + x2   
POL(AVG(x1)) = [2] + [5]x1   
POL(LENGTH(x1)) = [1] + [4]x1   
POL(QUOT(x1, x2)) = [2]   
POL(SUM(x1)) = [2] + x1   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c11(x1, x2)) = x1 + x2   
POL(c13(x1)) = x1   
POL(c3(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1, x2, x3)) = x1 + x2 + x3   
POL(c9(x1)) = x1   
POL(hd(x1)) = [2]   
POL(length(x1)) = [5] + [5]x1   
POL(nil) = 0   
POL(s(x1)) = 0   
POL(sum(x1)) = [1]   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c, c

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
We considered the (Usable) Rules:

sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
hd(:(z0, z1)) → z0
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = [5]   
POL(+'(x1, x2)) = [1]   
POL(++(x1, x2)) = [5]x2   
POL(++'(x1, x2)) = [2] + [5]x2   
POL(-(x1, x2)) = [2] + [2]x2   
POL(-'(x1, x2)) = 0   
POL(0) = [5]   
POL(:(x1, x2)) = [4] + x2   
POL(AVG(x1)) = [4] + [3]x1   
POL(LENGTH(x1)) = [1]   
POL(QUOT(x1, x2)) = [2]   
POL(SUM(x1)) = [1] + [2]x1   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c11(x1, x2)) = x1 + x2   
POL(c13(x1)) = x1   
POL(c3(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1, x2, x3)) = x1 + x2 + x3   
POL(c9(x1)) = x1   
POL(hd(x1)) = 0   
POL(length(x1)) = [5] + [3]x1   
POL(nil) = 0   
POL(s(x1)) = 0   
POL(sum(x1)) = [4]   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c, c

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
We considered the (Usable) Rules:

sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
hd(:(z0, z1)) → z0
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = x1 + x2   
POL(+'(x1, x2)) = 0   
POL(++(x1, x2)) = 0   
POL(++'(x1, x2)) = 0   
POL(-(x1, x2)) = x1   
POL(-'(x1, x2)) = 0   
POL(0) = [3]   
POL(:(x1, x2)) = x1 + x2   
POL(AVG(x1)) = [5] + [5]x1   
POL(LENGTH(x1)) = [3] + [4]x1   
POL(QUOT(x1, x2)) = [2]x1   
POL(SUM(x1)) = 0   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c11(x1, x2)) = x1 + x2   
POL(c13(x1)) = x1   
POL(c3(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1, x2, x3)) = x1 + x2 + x3   
POL(c9(x1)) = x1   
POL(hd(x1)) = x1   
POL(length(x1)) = [3] + [3]x1   
POL(nil) = [5]   
POL(s(x1)) = [2] + x1   
POL(sum(x1)) = [2] + [2]x1   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c6, c9, c11, c13, c, c

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3)))) by

SUM(++(x0, :(z0, :(z1, z2)))) → c6(SUM(++(x0, sum(:(+(z0, z1), z2)))), ++'(x0, sum(:(z0, :(z1, z2)))), SUM(:(z0, :(z1, z2))))
SUM(++(x0, :(x1, :(x2, x3)))) → c6(++'(x0, sum(:(x1, :(x2, x3)))))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
SUM(++(x0, :(z0, :(z1, z2)))) → c6(SUM(++(x0, sum(:(+(z0, z1), z2)))), ++'(x0, sum(:(z0, :(z1, z2)))), SUM(:(z0, :(z1, z2))))
SUM(++(x0, :(x1, :(x2, x3)))) → c6(++'(x0, sum(:(x1, :(x2, x3)))))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))
AVG(z0) → c
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
SUM(++(z0, :(z1, :(z2, z3)))) → c6(SUM(++(z0, sum(:(z1, :(z2, z3))))), ++'(z0, sum(:(z1, :(z2, z3)))), SUM(:(z1, :(z2, z3))))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c9, c11, c13, c, c, c6, c6

(19) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 3 of 12 dangling nodes:

AVG(z0) → c
AVG(z0) → c(SUM(z0))
AVG(z0) → c(LENGTH(z0))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
SUM(++(x0, :(z0, :(z1, z2)))) → c6(SUM(++(x0, sum(:(+(z0, z1), z2)))), ++'(x0, sum(:(z0, :(z1, z2)))), SUM(:(z0, :(z1, z2))))
SUM(++(x0, :(x1, :(x2, x3)))) → c6(++'(x0, sum(:(x1, :(x2, x3)))))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', QUOT, LENGTH, AVG

Compound Symbols:

c1, c3, c5, c9, c11, c13, c, c6, c6

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1)) by

QUOT(s(z0), s(0)) → c11(QUOT(z0, s(0)), -'(z0, 0))
QUOT(s(0), s(s(z0))) → c11(QUOT(0, s(s(z0))), -'(0, s(z0)))
QUOT(s(s(z0)), s(s(z1))) → c11(QUOT(-(z0, z1), s(s(z1))), -'(s(z0), s(z1)))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
SUM(++(x0, :(z0, :(z1, z2)))) → c6(SUM(++(x0, sum(:(+(z0, z1), z2)))), ++'(x0, sum(:(z0, :(z1, z2)))), SUM(:(z0, :(z1, z2))))
SUM(++(x0, :(x1, :(x2, x3)))) → c6(++'(x0, sum(:(x1, :(x2, x3)))))
QUOT(s(z0), s(0)) → c11(QUOT(z0, s(0)), -'(z0, 0))
QUOT(s(0), s(s(z0))) → c11(QUOT(0, s(s(z0))), -'(0, s(z0)))
QUOT(s(s(z0)), s(s(z1))) → c11(QUOT(-(z0, z1), s(s(z1))), -'(s(z0), s(z1)))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
QUOT(s(z0), s(z1)) → c11(QUOT(-(z0, z1), s(z1)), -'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', LENGTH, AVG, QUOT

Compound Symbols:

c1, c3, c5, c9, c13, c, c6, c6, c11

(23) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

SUM(++(x0, :(z0, :(z1, z2)))) → c6(SUM(++(x0, sum(:(+(z0, z1), z2)))), ++'(x0, sum(:(z0, :(z1, z2)))), SUM(:(z0, :(z1, z2))))
SUM(++(x0, :(x1, :(x2, x3)))) → c6(++'(x0, sum(:(x1, :(x2, x3)))))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
QUOT(s(z0), s(0)) → c11(QUOT(z0, s(0)), -'(z0, 0))
QUOT(s(0), s(s(z0))) → c11(QUOT(0, s(s(z0))), -'(0, s(z0)))
QUOT(s(s(z0)), s(s(z1))) → c11(QUOT(-(z0, z1), s(s(z1))), -'(s(z0), s(z1)))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', LENGTH, AVG, QUOT

Compound Symbols:

c1, c3, c5, c9, c13, c, c11

(25) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 1 of 9 dangling nodes:

QUOT(s(0), s(s(z0))) → c11(QUOT(0, s(s(z0))), -'(0, s(z0)))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
QUOT(s(z0), s(0)) → c11(QUOT(z0, s(0)), -'(z0, 0))
QUOT(s(s(z0)), s(s(z1))) → c11(QUOT(-(z0, z1), s(s(z1))), -'(s(z0), s(z1)))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', LENGTH, AVG, QUOT

Compound Symbols:

c1, c3, c5, c9, c13, c, c11

(27) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
QUOT(s(s(z0)), s(s(z1))) → c11(QUOT(-(z0, z1), s(s(z1))), -'(s(z0), s(z1)))
QUOT(s(z0), s(0)) → c11(QUOT(z0, s(0)))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', LENGTH, AVG, QUOT

Compound Symbols:

c1, c3, c5, c9, c13, c, c11, c11

(29) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

++'(:(z0, z1), z2) → c3(++'(z1, z2))
We considered the (Usable) Rules:

-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
hd(:(z0, z1)) → z0
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
QUOT(s(s(z0)), s(s(z1))) → c11(QUOT(-(z0, z1), s(s(z1))), -'(s(z0), s(z1)))
QUOT(s(z0), s(0)) → c11(QUOT(z0, s(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = [3]x1 + [3]x2   
POL(+'(x1, x2)) = 0   
POL(++(x1, x2)) = 0   
POL(++'(x1, x2)) = [3]x1   
POL(-(x1, x2)) = [2] + x1 + [5]x2   
POL(-'(x1, x2)) = 0   
POL(0) = 0   
POL(:(x1, x2)) = [1] + x2   
POL(AVG(x1)) = [2] + [5]x1   
POL(LENGTH(x1)) = 0   
POL(QUOT(x1, x2)) = [1]   
POL(SUM(x1)) = 0   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c11(x1)) = x1   
POL(c11(x1, x2)) = x1 + x2   
POL(c13(x1)) = x1   
POL(c3(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c9(x1)) = x1   
POL(hd(x1)) = [3]   
POL(length(x1)) = [3] + x1   
POL(nil) = [3]   
POL(s(x1)) = 0   
POL(sum(x1)) = [3] + x1   

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
QUOT(s(s(z0)), s(s(z1))) → c11(QUOT(-(z0, z1), s(s(z1))), -'(s(z0), s(z1)))
QUOT(s(z0), s(0)) → c11(QUOT(z0, s(0)))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', LENGTH, AVG, QUOT

Compound Symbols:

c1, c3, c5, c9, c13, c, c11, c11

(31) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

+'(s(z0), z1) → c1(+'(z0, z1))
We considered the (Usable) Rules:

-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
hd(:(z0, z1)) → z0
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
QUOT(s(s(z0)), s(s(z1))) → c11(QUOT(-(z0, z1), s(s(z1))), -'(s(z0), s(z1)))
QUOT(s(z0), s(0)) → c11(QUOT(z0, s(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = [1] + x1 + x2   
POL(+'(x1, x2)) = [2]x1   
POL(++(x1, x2)) = 0   
POL(++'(x1, x2)) = x1·x2   
POL(-(x1, x2)) = 0   
POL(-'(x1, x2)) = 0   
POL(0) = 0   
POL(:(x1, x2)) = [2] + x1 + x2   
POL(AVG(x1)) = [2] + x1 + [2]x12   
POL(LENGTH(x1)) = [2]x1   
POL(QUOT(x1, x2)) = [1]   
POL(SUM(x1)) = x12   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c11(x1)) = x1   
POL(c11(x1, x2)) = x1 + x2   
POL(c13(x1)) = x1   
POL(c3(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c9(x1)) = x1   
POL(hd(x1)) = 0   
POL(length(x1)) = 0   
POL(nil) = 0   
POL(s(x1)) = [1] + x1   
POL(sum(x1)) = 0   

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
QUOT(s(s(z0)), s(s(z1))) → c11(QUOT(-(z0, z1), s(s(z1))), -'(s(z0), s(z1)))
QUOT(s(z0), s(0)) → c11(QUOT(z0, s(0)))
S tuples:

-'(s(z0), s(z1)) → c9(-'(z0, z1))
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
+'(s(z0), z1) → c1(+'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', LENGTH, AVG, QUOT

Compound Symbols:

c1, c3, c5, c9, c13, c, c11, c11

(33) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

-'(s(z0), s(z1)) → c9(-'(z0, z1))
We considered the (Usable) Rules:

-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
hd(:(z0, z1)) → z0
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
QUOT(s(s(z0)), s(s(z1))) → c11(QUOT(-(z0, z1), s(s(z1))), -'(s(z0), s(z1)))
QUOT(s(z0), s(0)) → c11(QUOT(z0, s(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = x1 + x2   
POL(+'(x1, x2)) = 0   
POL(++(x1, x2)) = 0   
POL(++'(x1, x2)) = x1·x2   
POL(-(x1, x2)) = x1   
POL(-'(x1, x2)) = x2   
POL(0) = 0   
POL(:(x1, x2)) = [2] + x1 + x2   
POL(AVG(x1)) = [3] + [2]x12   
POL(LENGTH(x1)) = [2]x1 + [3]x12   
POL(QUOT(x1, x2)) = x1·x2   
POL(SUM(x1)) = 0   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c11(x1)) = x1   
POL(c11(x1, x2)) = x1 + x2   
POL(c13(x1)) = x1   
POL(c3(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c9(x1)) = x1   
POL(hd(x1)) = [2]x1   
POL(length(x1)) = x1   
POL(nil) = 0   
POL(s(x1)) = [2] + x1   
POL(sum(x1)) = x1   

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
++(nil, z0) → z0
++(:(z0, z1), z2) → :(z0, ++(z1, z2))
sum(:(z0, nil)) → :(z0, nil)
sum(:(z0, :(z1, z2))) → sum(:(+(z0, z1), z2))
sum(++(z0, :(z1, :(z2, z3)))) → sum(++(z0, sum(:(z1, :(z2, z3)))))
-(z0, 0) → z0
-(0, s(z0)) → 0
-(s(z0), s(z1)) → -(z0, z1)
quot(0, s(z0)) → 0
quot(s(z0), s(z1)) → s(quot(-(z0, z1), s(z1)))
length(nil) → 0
length(:(z0, z1)) → s(length(z1))
hd(:(z0, z1)) → z0
avg(z0) → quot(hd(sum(z0)), length(z0))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
QUOT(s(s(z0)), s(s(z1))) → c11(QUOT(-(z0, z1), s(s(z1))), -'(s(z0), s(z1)))
QUOT(s(z0), s(0)) → c11(QUOT(z0, s(0)))
S tuples:none
K tuples:

AVG(z0) → c(QUOT(hd(sum(z0)), length(z0)))
LENGTH(:(z0, z1)) → c13(LENGTH(z1))
SUM(:(z0, :(z1, z2))) → c5(SUM(:(+(z0, z1), z2)), +'(z0, z1))
++'(:(z0, z1), z2) → c3(++'(z1, z2))
+'(s(z0), z1) → c1(+'(z0, z1))
-'(s(z0), s(z1)) → c9(-'(z0, z1))
Defined Rule Symbols:

+, ++, sum, -, quot, length, hd, avg

Defined Pair Symbols:

+', ++', SUM, -', LENGTH, AVG, QUOT

Compound Symbols:

c1, c3, c5, c9, c13, c, c11, c11

(35) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(36) BOUNDS(O(1), O(1))